CHOICE-STRATEGY-IS: 
@(SUPPORT C2);

EDIT-STRATEGY-IS: 
α(C)>1∨∂(C)>3;


PARMODULATE =T
EQUAL-SYMBOL ==
PAR-DEPTH-BOUND =101
ELAPSED-TIME =5983

NIL 1 3
1 ¬(THEOREM1 ⊗(THEOREM3 ⊗(THEOREM2 ⊗ THEOREM1)))=(THEOREM2 ⊗ THEOREM3);3 4
3 (x ⊗(y ⊗ z))=(z ⊗(y ⊗ x));G3
4 ¬((THEOREM2 ⊗ THEOREM1)⊗(THEOREM3 ⊗ THEOREM1))=(THEOREM2 ⊗ THEOREM3);THEOREM